/*
 * Atomic Predicates for Transformers
 * 
 * Copyright (c) 2015 UNIVERSITY OF TEXAS AUSTIN. All rights reserved. Developed
 * by: HONGKUN YANG and SIMON S. LAM http://www.cs.utexas.edu/users/lam/NRL/
 * 
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * with the Software without restriction, including without limitation the
 * rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
 * sell copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 * 
 * 1. Redistributions of source code must retain the above copyright notice,
 * this list of conditions and the following disclaimers.
 * 
 * 2. Redistributions in binary form must reproduce the above copyright notice,
 * this list of conditions and the following disclaimers in the documentation
 * and/or other materials provided with the distribution.
 * 
 * 3. Neither the name of the UNIVERSITY OF TEXAS AUSTIN nor the names of the
 * developers may be used to endorse or promote products derived from this
 * Software without specific prior written permission.
 * 
 * 4. Any report or paper describing results derived from using any part of this
 * Software must cite the following publication of the developers: Hongkun Yang
 * and Simon S. Lam, Scalable Verification of Networks With Packet Transformers
 * Using Atomic Predicates, IEEE/ACM Transactions on Networking, October 2017,
 * Volume 25, No. 5, pages 2900-2915 (first published as IEEE Early Access
 * Article, July 2017, Digital Object Identifier: 10.1109/TNET.2017.2720172).
 * 
 * 
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * CONTRIBUTORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS WITH
 * THE SOFTWARE.
 */
package transformer;

import java.io.*;
import java.util.*;

import common.BDDACLWrapper;
import common.Fields;
import common.PositionTuple;

public class NetworkStanford extends Net{

    /**
     * 
     */
    private static final long serialVersionUID = 2178831997990684032L;
    HashMap<String, ArrayList<String>> unused_ports;
    int max_unused_ports_per_router = 100;


    public void add_nat_each_edge(int nat_num)
    {
        int cnt = 0;
        for(int j = 0; j < nat_num; j ++)
        {
            for(int i = 0; i < edgerouters.size(); i++)
            {
                DeviceStanford d = (DeviceStanford) boxes.get(edgerouters.get(i));
                PositionTuple pt_r = d.add_nat();

                NATBox nat = new NATBox("nat"+cnt);
                nat.add_entry_out(BDDACLWrapper.BDDTrue, bddengine.get_field_bdd(Fields.dst_ip), 
                        bddengine.encodeDstIPPrefix(12345678L, 32));

                PositionTuple pt_nat = new PositionTuple(nat.getName(), NATBox.port_out);
                addTopology(pt_r, pt_nat);
                addBox(nat);

                cnt ++;
            }
        }
    }

    public NetworkStanford() throws IOException
    {
        name = "Stanford";
        bddengine = new BDDACLWrapper();

        boxes = new HashMap<String, Box> ();
        Box.setBDDWrapper(bddengine);

        BuildNetwork.set_al2s(false);

        String foldername2 = "st/";
        String foldername1 = "stconfig/";
        String [] devicenames = {"bbra_rtr", "bbrb_rtr", "boza_rtr", "bozb_rtr", "coza_rtr", "cozb_rtr", "goza_rtr",
                "gozb_rtr", "poza_rtr", "pozb_rtr", "roza_rtr", "rozb_rtr", "soza_rtr", "sozb_rtr", "yoza_rtr", "yozb_rtr"};


        edgerouters = new ArrayList<String>(Arrays.asList(new String []{"boza_rtr", "bozb_rtr", "coza_rtr", "cozb_rtr", "goza_rtr",
                "gozb_rtr", "poza_rtr", "pozb_rtr", "roza_rtr", "rozb_rtr", "soza_rtr", "sozb_rtr", 
                "yoza_rtr", "yozb_rtr"}));

        for( int i = 0; i < devicenames.length; i ++)
        {
            DeviceStanford d = BuildNetwork.parseDeviceStanford(devicenames[i], foldername1 + devicenames[i] + "_config.txt"
                    , foldername2 + devicenames[i] + "ap");


            System.out.println(d.name);
            boxes.put(d.name, d);
            //d.show_fwd_bddsize();
        }

        for(Box b : boxes.values())
        {
            DeviceStanford d = (DeviceStanford) b;
            d.computeFWBDDs();
            d.computeACLBDDs();
        }

        topology = new HashMap<PositionTuple, HashSet<PositionTuple>> ();

        addTopology("bbra_rtr","te7/3","goza_rtr","te2/1");
        addTopology("bbra_rtr","te7/3","pozb_rtr","te3/1");
        addTopology("bbra_rtr","te1/3","bozb_rtr","te3/1");
        addTopology("bbra_rtr","te1/3","yozb_rtr","te2/1");
        addTopology("bbra_rtr","te1/3","roza_rtr","te2/1");
        addTopology("bbra_rtr","te1/4","boza_rtr","te2/1");
        addTopology("bbra_rtr","te1/4","rozb_rtr","te3/1");
        addTopology("bbra_rtr","te6/1","gozb_rtr","te3/1");
        addTopology("bbra_rtr","te6/1","cozb_rtr","te3/1");
        addTopology("bbra_rtr","te6/1","poza_rtr","te2/1");
        addTopology("bbra_rtr","te6/1","soza_rtr","te2/1");
        addTopology("bbra_rtr","te7/2","coza_rtr","te2/1");
        addTopology("bbra_rtr","te7/2","sozb_rtr","te3/1");
        addTopology("bbra_rtr","te6/3","yoza_rtr","te1/3");
        addTopology("bbra_rtr","te7/1","bbrb_rtr","te7/1");
        addTopology("bbrb_rtr","te7/4","yoza_rtr","te7/1");
        addTopology("bbrb_rtr","te1/1","goza_rtr","te3/1");
        addTopology("bbrb_rtr","te1/1","pozb_rtr","te2/1");
        addTopology("bbrb_rtr","te6/3","bozb_rtr","te2/1");
        addTopology("bbrb_rtr","te6/3","roza_rtr","te3/1");
        addTopology("bbrb_rtr","te6/3","yozb_rtr","te1/1");
        addTopology("bbrb_rtr","te1/3","boza_rtr","te3/1");
        addTopology("bbrb_rtr","te1/3","rozb_rtr","te2/1");
        addTopology("bbrb_rtr","te7/2","gozb_rtr","te2/1");
        addTopology("bbrb_rtr","te7/2","cozb_rtr","te2/1");
        addTopology("bbrb_rtr","te7/2","poza_rtr","te3/1");
        addTopology("bbrb_rtr","te7/2","soza_rtr","te3/1");
        addTopology("bbrb_rtr","te6/1","coza_rtr","te3/1");
        addTopology("bbrb_rtr","te6/1","sozb_rtr","te2/1");
        addTopology("boza_rtr","te2/3","bozb_rtr","te2/3");
        addTopology("coza_rtr","te2/3","cozb_rtr","te2/3");
        addTopology("goza_rtr","te2/3","gozb_rtr","te2/3");
        addTopology("poza_rtr","te2/3","pozb_rtr","te2/3");
        addTopology("roza_rtr","te2/3","rozb_rtr","te2/3");
        addTopology("soza_rtr","te2/3","sozb_rtr","te2/3");   
        addTopology("yoza_rtr","te1/1","yozb_rtr","te1/3");
        addTopology("yoza_rtr","te1/2","yozb_rtr","te1/2");

        int num_links = 0;
        for(PositionTuple port : topology.keySet())
        {
            num_links += topology.get(port).size();
        }
        System.out.println(num_links + "/2 links.");

        setactiveports();
        System.out.println(getallactiveports().size() + " ports");

        unused_ports = new HashMap<String, ArrayList<String>> ();
        for(String r : edgerouters)
        {
            Box d = boxes.get(r);
            Set<String> ports = ((DeviceStanford) d).fwbdds.keySet();
            for(String port : ports)
            {
                PositionTuple pt = new PositionTuple(d.getName(), port);
                if(!topology.containsKey(pt))
                {
                    if(!unused_ports.containsKey(d.getName()))
                    {
                        unused_ports.put(d.getName(), new ArrayList<String>()); 
                    }
                    unused_ports.get(d.getName()).add(port);
                }
            }
        }

        for(String router : unused_ports.keySet())
        {
            if(max_unused_ports_per_router > unused_ports.get(router).size())
            {
                max_unused_ports_per_router = unused_ports.get(router).size();
            }
        }

        System.out.println(unused_ports.size() + " edge routers.");
        System.out.println(max_unused_ports_per_router + " NATs per router.");

        for(String r : edgerouters)
        {
            DeviceStanford d = (DeviceStanford) boxes.get(r);
            Set<String> usedports = d.fwbdds.keySet();
            for(String port: usedports)
            {
                if(!port.equals("self"))
                {
                    PositionTuple pt = new PositionTuple(r, port);
                    if((!topology.containsKey(pt))&&d.find_nat_subnet_minlen(port, 25))
                    {
                        System.out.println(d.name);
                        System.out.println("find nat prefix");
                        break;
                    }
                }
            }

        }

        // save to file
        /*
            PrintWriter pw = new PrintWriter(new File(name+"_nat"));
            for(String r : edgerouters)
            {
                  Device d = (Device) boxes.get(r);
                  pw.println(d.name+" " + d.nat_addr);
            }
            pw.close();
         */
    }

    public static void main(String[] args) throws IOException
    {
        long t1 = System.currentTimeMillis();
        NetworkStanford ns = new NetworkStanford();
        long t2 = System.currentTimeMillis();
        System.out.println("preprocessing time takes " + (t2-t1) + " ms");
    }
}
